\begin{tabbing}
$\forall$\=$k$:Knd, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it mTyp}$, ${\it vTyp}$:Type, $l$:IdLnk, ${\it tg}$:Id,\+
\\[0ex]$f$:((:State(${\it ds}$) $\times$ ${\it vTyp}$)$\rightarrow$(${\it mTyp}$ + Top)), ${\it es}$:ES.
\-\\[0ex]sends $k$(v:${\it vTyp}$) on $l$:
\\[0ex]tagged([\=$<$${\it tg}$\+
\\[0ex], $\lambda$$s$,$v$. if can{-}apply($f$;$<$$s$, $v$$>$) then [do{-}apply($f$;$<$$s$, $v$$>$)] else [] fi 
\\[0ex]$>$],State(${\it ds}$),v):if isrcvl($l$;$k$) then ${\it tg}$ : ${\it mTyp}$ $\oplus$ tag($k$) : ${\it vTyp}$ else ${\it tg}$ : ${\it mTyp}$ fi 
\-\\[0ex]$\Rightarrow$ $k$(v:${\it vTyp}$) sends on $l$ [${\it tg}$:${\it mTyp}$, $f$ $<$state, v$>$]?[]
\end{tabbing}